T:Type, L:T List, R:(||L||||L||Prop), P1, P2, P3:(||L||Prop).
(Trans _1,_2:||L||. R(_1,_2))
 causal_order(L;R;P1;P2)
 causal_order(L;R;P2;P3)
 causal_order(L;R;P1;P3) 

latex

Definitions	t  T, P  Q, x:A. B(x), Trans x,y:T. E(x;y), {i..j}, AB, Prop, P & Q, ij, ||as||, x:A. B(x), x,y. t(x;y), False, A, i  j < k, causal_order(L;R;P;Q)
Lemmas	trans wf, int seg wf, length wf1, le wf